(declare-fun a () String)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(declare-fun e () Int)
(assert (or (> b 9) (<= c 51) (> (+ 6 b c) (str.len a))))
(assert (and (<= d 95) (> e 88) (>= (* d e) (str.len a))))
(assert (= "efg" (str.substr a b c)))
(assert (= "bef" (str.substr a d e)))
(assert (> (str.len a) 12))
(check-sat)
